Nuprl Lemma : s-out-declared_wf 0,22
i:Id, d:OutDecl(i), p:(IdLnkId). d(p)  Type 
latex

Definitionsx:A. B(x), OutDecl(i), t  T, d(p), x. t(x), Prop, x(s)
Lemmasfpf-cap wf, IdLnk wf, Id wf, fpf-trivial-subtype-set, lsrc wf, pi1 wf, product-deq wf, idlnk-deq wf, id-deq wf, top wf, fpf wf

origin